/*
 * RFact.h
 *
 *  Created on: Jul 8, 2012
 *      Author: kobe
 */

#ifndef RFACT_H_
#define RFACT_H_

#include "Rule.h"

class R_Fact: public Rule {
public:
	R_Fact(AtomicProposition*, AtomicAction*, Proposition*);
	virtual ~R_Fact();
	std::string toString();
	std::vector<Sequent*> run(Sequent*);
	std::string toLatex();
	RuleType getRuleType();
private:
	AtomicProposition* mProp;
	AtomicAction* mAction;
	Proposition* mPropPrime;
	Context* search(Context*);
};

#endif /* RFACT_H_ */
